(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 8))
(declare-fun v1 () (_ BitVec 15))
(declare-fun v2 () (_ BitVec 11))
(declare-fun v3 () (_ BitVec 16))
(assert (let ((e4(_ bv3 4)))
(let ((e5 (bvurem v1 v1)))
(let ((e6 (bvshl ((_ sign_extend 8) v0) v3)))
(let ((e7 (ite (bvult v3 v3) (_ bv1 1) (_ bv0 1))))
(let ((e8 (bvcomp v1 ((_ zero_extend 14) e7))))
(let ((e9 (ite (bvslt v1 ((_ zero_extend 4) v2)) (_ bv1 1) (_ bv0 1))))
(let ((e10 (ite (bvult e6 ((_ zero_extend 5) v2)) (_ bv1 1) (_ bv0 1))))
(let ((e11 (bvxnor v0 ((_ sign_extend 7) e8))))
(let ((e12 (ite (bvsgt v3 ((_ sign_extend 5) v2)) (_ bv1 1) (_ bv0 1))))
(let ((e13 (bvshl ((_ sign_extend 8) e11) v3)))
(let ((e14 (bvsdiv ((_ sign_extend 14) e7) v1)))
(let ((e15 (bvshl e5 v1)))
(let ((e16 ((_ sign_extend 0) v0)))
(let ((e17 (bvmul v2 ((_ sign_extend 10) e10))))
(let ((e18 (bvudiv e7 e8)))
(let ((e19 (ite (bvule e8 e9) (_ bv1 1) (_ bv0 1))))
(let ((e20 (bvshl e8 e10)))
(let ((e21 (ite (= (_ bv1 1) ((_ extract 0 0) e7)) ((_ zero_extend 1) v1) e13)))
(let ((e22 (bvnand ((_ sign_extend 8) e16) e13)))
(let ((e23 (ite (bvugt e9 e19) (_ bv1 1) (_ bv0 1))))
(let ((e24 (ite (= (_ bv1 1) ((_ extract 12 12) e13)) e21 ((_ sign_extend 15) e12))))
(let ((e25 (bvudiv ((_ sign_extend 1) e15) e6)))
(let ((e26 (bvsub e22 ((_ zero_extend 15) e10))))
(let ((e27 (bvmul e24 ((_ sign_extend 12) e4))))
(let ((e28 (bvule ((_ zero_extend 10) e19) e17)))
(let ((e29 (bvsle e10 e18)))
(let ((e30 (bvugt e5 ((_ sign_extend 7) e16))))
(let ((e31 (bvsle ((_ sign_extend 15) e10) e6)))
(let ((e32 (bvslt e14 ((_ zero_extend 4) v2))))
(let ((e33 (bvsgt ((_ sign_extend 15) e8) e21)))
(let ((e34 (= e6 ((_ zero_extend 15) e18))))
(let ((e35 (distinct e24 e13)))
(let ((e36 (bvugt ((_ zero_extend 8) e16) v3)))
(let ((e37 (bvule e5 v1)))
(let ((e38 (bvuge e24 e27)))
(let ((e39 (bvult e4 ((_ sign_extend 3) e7))))
(let ((e40 (bvsgt e26 ((_ sign_extend 15) e23))))
(let ((e41 (bvsle v0 v0)))
(let ((e42 (bvugt e21 e6)))
(let ((e43 (distinct e27 ((_ zero_extend 15) e12))))
(let ((e44 (bvugt ((_ zero_extend 12) e4) e24)))
(let ((e45 (bvsle e26 e26)))
(let ((e46 (bvult e19 e12)))
(let ((e47 (bvule e5 ((_ zero_extend 7) e16))))
(let ((e48 (bvsle v2 ((_ zero_extend 10) e23))))
(let ((e49 (bvsge e18 e8)))
(let ((e50 (bvule e17 ((_ sign_extend 10) e9))))
(let ((e51 (bvugt e16 ((_ zero_extend 7) e23))))
(let ((e52 (bvsgt ((_ sign_extend 12) e4) v3)))
(let ((e53 (distinct e5 ((_ zero_extend 14) e8))))
(let ((e54 (bvugt ((_ sign_extend 8) e16) e26)))
(let ((e55 (bvule ((_ sign_extend 4) e17) e15)))
(let ((e56 (= ((_ sign_extend 15) e9) e26)))
(let ((e57 (bvule v3 ((_ sign_extend 12) e4))))
(let ((e58 (distinct ((_ sign_extend 15) e23) e6)))
(let ((e59 (distinct e27 v3)))
(let ((e60 (bvsgt ((_ zero_extend 11) e4) e14)))
(let ((e61 (= e25 ((_ sign_extend 15) e10))))
(let ((e62 (bvsgt e14 ((_ zero_extend 7) v0))))
(let ((e63 (bvule e11 ((_ zero_extend 7) e23))))
(let ((e64 (bvsgt e11 ((_ sign_extend 7) e12))))
(let ((e65 (bvsgt v3 ((_ sign_extend 5) v2))))
(let ((e66 (bvugt e27 e6)))
(let ((e67 (bvsle e9 e7)))
(let ((e68 (distinct ((_ zero_extend 15) e12) v3)))
(let ((e69 (bvsge ((_ sign_extend 14) e23) e5)))
(let ((e70 (bvslt e25 e22)))
(let ((e71 (bvule e11 e16)))
(let ((e72 (bvugt v3 ((_ sign_extend 15) e18))))
(let ((e73 (bvugt e22 ((_ zero_extend 15) e9))))
(let ((e74 (bvugt e4 ((_ zero_extend 3) e10))))
(let ((e75 (bvslt e10 e18)))
(let ((e76 (bvsle ((_ zero_extend 14) e23) v1)))
(let ((e77 (bvsle ((_ sign_extend 15) e9) e6)))
(let ((e78 (bvule ((_ sign_extend 15) e19) e21)))
(let ((e79 (bvult e20 e20)))
(let ((e80 (ite e29 e71 e61)))
(let ((e81 (not e75)))
(let ((e82 (and e53 e38)))
(let ((e83 (ite e78 e59 e80)))
(let ((e84 (=> e56 e46)))
(let ((e85 (xor e54 e83)))
(let ((e86 (=> e49 e41)))
(let ((e87 (= e52 e67)))
(let ((e88 (not e31)))
(let ((e89 (and e81 e84)))
(let ((e90 (= e48 e48)))
(let ((e91 (or e89 e64)))
(let ((e92 (ite e55 e88 e42)))
(let ((e93 (not e40)))
(let ((e94 (xor e74 e58)))
(let ((e95 (and e90 e90)))
(let ((e96 (=> e57 e92)))
(let ((e97 (and e62 e76)))
(let ((e98 (and e47 e95)))
(let ((e99 (and e68 e60)))
(let ((e100 (and e72 e99)))
(let ((e101 (not e94)))
(let ((e102 (not e100)))
(let ((e103 (=> e37 e73)))
(let ((e104 (xor e91 e44)))
(let ((e105 (xor e82 e45)))
(let ((e106 (and e28 e36)))
(let ((e107 (= e32 e63)))
(let ((e108 (xor e86 e98)))
(let ((e109 (=> e43 e33)))
(let ((e110 (= e79 e109)))
(let ((e111 (xor e39 e77)))
(let ((e112 (ite e101 e87 e105)))
(let ((e113 (and e50 e107)))
(let ((e114 (= e85 e110)))
(let ((e115 (=> e112 e102)))
(let ((e116 (not e111)))
(let ((e117 (not e108)))
(let ((e118 (= e69 e93)))
(let ((e119 (and e96 e34)))
(let ((e120 (ite e106 e30 e35)))
(let ((e121 (not e117)))
(let ((e122 (and e66 e65)))
(let ((e123 (xor e120 e51)))
(let ((e124 (xor e118 e70)))
(let ((e125 (or e123 e122)))
(let ((e126 (=> e113 e113)))
(let ((e127 (= e103 e103)))
(let ((e128 (=> e114 e116)))
(let ((e129 (and e104 e115)))
(let ((e130 (= e127 e127)))
(let ((e131 (xor e126 e119)))
(let ((e132 (not e124)))
(let ((e133 (= e125 e97)))
(let ((e134 (xor e132 e133)))
(let ((e135 (xor e129 e131)))
(let ((e136 (xor e128 e135)))
(let ((e137 (xor e136 e130)))
(let ((e138 (or e121 e134)))
(let ((e139 (or e137 e138)))
(let ((e140 (and e139 (not (= e8 (_ bv0 1))))))
(let ((e141 (and e140 (not (= v1 (_ bv0 15))))))
(let ((e142 (and e141 (not (= v1 (bvnot (_ bv0 15)))))))
(let ((e143 (and e142 (not (= e6 (_ bv0 16))))))
e143
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
